A, B:MsgA. A = B  ma-frame-compat(B;B)  (B ||+ A) 

latex

Definitions	x:AB(x), ma-frame-compat(A;B), P & Q, ma-frame-compatible(A;B), t  T, x:A. B(x), M1 || M2, A ||+ B, MsgA, s = t, Prop, P  Q
Lemmas	ma-frame-compat wf, msga wf, ma-compat wf, ma-compatible-self